Nuprl Lemma : R-size-implies
0,22
postcript
pdf
R
:Realizer.
1<R-size(
R
)
(
A
,
B
:Realizer.
R
= (
A
B
) & R-size(
A
)<R-size(
R
) & R-size(
B
)<R-size(
R
))
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
R-size(
R
)
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
Prop
,
x
.
t
(
x
)
,
t
T
,
x
,
y
,
z
,
w
.
t
(
x
;
y
;
z
;
w
)
,
x
,
y
,
z
.
t
(
x
;
y
;
z
)
,
x
,
y
,
z
,
u
,
v
,
w
.
t
(
x
;
y
;
z
;
u
;
v
;
w
)
,
x
,
y
,
z
,
w
,
v
.
t
(
x
;
y
;
z
;
w
;
v
)
,
x
(
s
)
,
{
T
}
,
x
(
s1
,
s2
,
s3
,
s4
)
,
x
(
s1
,
s2
,
s3
)
,
x
(
a
,
b
,
c
,
d
,
e
,
f
)
,
x
(
s1
,
s2
,
s3
,
s4
,
s5
)
,
Lemmas
es
realizer-induction
,
es
realizer
ind
wf
,
es
realizer
wf
,
Id
wf
,
Knd
wf
,
IdLnk
wf
,
decl-state
wf
,
decl-type
wf
,
fpf
wf
,
Rplus
wf
,
R-size
wf
,
nat
plus
wf
origin
R:Realizer.
(
A, B:Realizer. R = (A 
B) & R-size(A)<R-size(R) & R-size(B)<R-size(R)) R:Realizer.
(A, B:Realizer. R = (A B) & R-size(A)<R-size(R) & R-size(B)<R-size(R)) 
x. t(x)
T
